(SETQ IBASE (ADD1 7)) 


(DEFPROP DIFF 
 (LAMBDA(E V)
  (COND ((ATOM E) (COND ((EQ E V) 1) (T 0)))
	((EQ (CAR E) (QUOTE PLUS)) (CONS (QUOTE PLUS) (DPLUS (CDR E) V)))
	((EQ (CAR E) (QUOTE MINUS)) (LIST (QUOTE MINUS) (DIFF (CADR E) V)))
	((EQ (CAR E) (QUOTE TIMES))
	 (CONS (QUOTE PLUS)
	       (MAPLIST (FUNCTION
			 (LAMBDA(X)
			  (CONS (QUOTE TIMES)
				(MAPLIST (FUNCTION (LAMBDA (Y) (COND ((EQ X Y) (DIFF (CAR Y) V)) (T (CAR Y)))))
					 (CDR E)))))
			(CDR E)))))) 
EXPR)

(DEFPROP DIFF 
 (NIL DIFFA DIFF DPLUS SIMP SIMP1 SPLUS STIMES) 
VALUE)

(DEFPROP DIFFA 
 (LAMBDA (L) (PROG NIL L (TERPRI) (OUT (QUOTE >EXPR<) (SIMP (DIFF (IN <EXPR>) (CAR L)))) (GO L))) 
FEXPR)

(DEFPROP DIFF 
 (LAMBDA(E V)
  (COND ((ATOM E) (COND ((EQ E V) 1) (T 0)))
	((EQ (CAR E) (QUOTE PLUS)) (CONS (QUOTE PLUS) (DPLUS (CDR E) V)))
	((EQ (CAR E) (QUOTE MINUS)) (LIST (QUOTE MINUS) (DIFF (CADR E) V)))
	((EQ (CAR E) (QUOTE TIMES))
	 (CONS (QUOTE PLUS)
	       (MAPLIST (FUNCTION
			 (LAMBDA(X)
			  (CONS (QUOTE TIMES)
				(MAPLIST (FUNCTION (LAMBDA (Y) (COND ((EQ X Y) (DIFF (CAR Y) V)) (T (CAR Y)))))
					 (CDR E)))))
			(CDR E)))))) 
EXPR)

(DEFPROP DIFF 
 (NIL DIFFA DIFF DPLUS SIMP SIMP1 SPLUS STIMES) 
VALUE)

(DEFPROP DPLUS 
 (LAMBDA (U V) (COND ((NULL U) NIL) (T (CONS (DIFF (CAR U) V) (DPLUS (CDR U) V))))) 
EXPR)

(DEFPROP SIMP 
 (LAMBDA(U)
  (COND ((ATOM U) U)
	(T
	 ((LAMBDA (W) (COND ((EQUAL W U) U) (T (SIMP W))))
	  (SIMP1 (CONS (CAR U) (MAPLIST (FUNCTION (LAMBDA (Z) (SIMP (CAR Z)))) (CDR U)))))))) 
EXPR)

(DEFPROP SIMP1 
 (LAMBDA(E)
  (COND
   ((EQ (CAR E) (QUOTE MINUS))
    (COND ((AND (NOT (ATOM (CADR E))) (EQ (CAADR E) (QUOTE MINUS))) (CADADR E)) (T E)))
   ((EQ (CAR E) (QUOTE PLUS))
    ((LAMBDA (W) (COND ((NULL W) 0) ((NULL (CDR W)) (CAR W)) (T (CONS (QUOTE PLUS) W)))) (SPLUS (CDR E))))
   ((EQ (CAR E) (QUOTE TIMES))
    ((LAMBDA (W) (COND ((NULL W) 1) ((EQ W (QUOTE NO)) 0) ((NULL (CDR W)) (CAR W)) (T (CONS (QUOTE TIMES) W))))
     (STIMES (CDR E)))))) 
EXPR)

(DEFPROP SPLUS 
 (LAMBDA (U) (COND ((NULL U) NIL) ((EQ (CAR U) 0) (SPLUS (CDR U))) (T (CONS (CAR U) (SPLUS (CDR U)))))) 
EXPR)

(DEFPROP STIMES 
 (LAMBDA(U)
  (COND ((NULL U) NIL)
	(T
	 ((LAMBDA(W)
	   (COND ((EQ W (QUOTE NO)) W) ((EQ (CAR U) 0) (QUOTE NO)) ((EQ (CAR U) 1) W) (T (CONS (CAR U) W))))
	  (STIMES (CDR U)))))) 
EXPR)